\documentclass[a4paper,12pt]{article}

\usepackage[francais]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{multicol}

\title{Logique et programmation logique}
\author{Julien Gamba}

\begin{document}

\maketitle

Si $\models F$, alors $\models F [p:=G]$.
\begin{proof}
Montrons que pour toute interprétation $I$, 

$I(F[p:=G])=1$.

Soit $I$ une interprétation satisfaisant $\models F [p:=G]$.

Soit $J$ l'interprétation telle que 
$\left\{
\begin{array}{l}
J(p)=I(G) \\
J(q)=I(q)
\end{array}
\right.$
, quelque soit $q\neq p$.

On en déduit que : $I(F(p:=G))=J(F)$

Or, $\models F$. Donc : $J(F)=1$. D'o\'u $I(F(p:=G))=1$. On en conclue
que :
\[\boxed{\models F(p:=G)}\]
\end{proof}

Si $F \equiv F'$, alors $F[p:=G]\equiv F'[p:=G]$.
\begin{proof}
Soit $A$ une formule telle que : $A=(F\Leftrightarrow F')$.

$\begin{array}{l l l}
F\equiv F' & \text{ssi} & \models(F\Leftrightarrow F') \\
& \text{ssi} & \models A
\end{array}$

On veut montrer que : $\models A$

Montrons que : $\models A[p:=G]$, donc que $\models(F\Leftrightarrow F')[p:=G]$.

\vspace{10pt}
$\begin{array}{l l}
\models(F\Leftrightarrow F')[p:=G] & \models((F\Rightarrow F') \wedge (F'\Rightarrow F))[p:=G] \\
& \models(F\Rightarrow F'[p:=G] \wedge F'\Rightarrow F[p:=G]) \\
& \models F[p:=G]\Rightarrow F'[p:=G] \wedge F'[p:=G]\Rightarrow F[p:=G] \\
& \models F[p:=G] \Leftrightarrow F'[p:=G] \\
\end{array}$

On en déduit que :
\[\boxed{F[p:=G]\equiv F'[p:=G]}\]
\end{proof}

Si $G\equiv G'$, alors $F[p:=G]\equiv F[p:=G']$.
\begin{proof}

\end{proof}
\end{document}
